\begin{tabbing}
valid{-}sys(${\it es}$;${\it Config}$;${\it Sys}$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=chain\_sys\_ind(${\it Sys}$($e$);$x$.$\exists$$c$$<$$e$.($\uparrow$($c$ $\in_{b}$ ${\it Config}$)) \& ($\uparrow$cchead?(${\it Config}$($c$)))\+
\\[0ex]\& \=$\exists$$c$$<$$e$.($\uparrow$($c$ $\in_{b}$ ${\it Config}$))\+
\\[0ex]\& (($\uparrow$cctail?(${\it Config}$($c$))) $\vee$ ($\uparrow$ccsucc?(${\it Config}$($c$))));$i$,${\it xs}$.$\exists$$c$$<$$e$.($\uparrow$($c$ $\in_{b}$ ${\it Config}$))
\-\\[0ex]\& ($\uparrow$ccpred?(${\it Config}$($c$)))
\\[0ex]\& ccpred{-}id(${\it Config}$($c$)) = $i$
\\[0ex]\& ($\forall$${\it e'}$$<$$e$. ($c$ $<$loc ${\it e'}$) $\Rightarrow$ ($\neg$(($\uparrow$(${\it e'}$ $\in_{b}$ ${\it Config}$)) \& ($\uparrow$ccpred?(${\it Config}$(${\it e'}$)))))))
\-
\end{tabbing}